#include "driver_instrumentation.h"
#include "wdf.h"
#include "instrumentation.h"
#include "storm_driver_entries.h"
#include "dispatch_routines.h"


void dispatch() {
#if DISPATCH == 0
  #ifdef storm_WDF_IO_QUEUE_IO_DEFAULT
    storm_WDF_IO_QUEUE_IO_DEFAULT((WDFQUEUE)&hqueue,&hrequest);
  #elif
    #error Function WDF_IO_QUEUE_IO_DEFAULT not defined
  #endif

#elif DISPATCH == 1
  #ifdef storm_WDF_IO_QUEUE_IO_READ
    storm_WDF_IO_QUEUE_IO_READ((WDFQUEUE)&hqueue,&hrequest,(size_t)storm_nondet());
  #elif
    #error Function WDF_IO_QUEUE_IO_READ not defined
  #endif

#elif DISPATCH == 2
  #ifdef storm_WDF_IO_QUEUE_IO_WRITE
    storm_WDF_IO_QUEUE_IO_WRITE((WDFQUEUE)&hqueue,&hrequest,(size_t)storm_nondet());
  #elif
    #error Function WDF_IO_QUEUE_IO_WRITE not defined
  #endif

#elif DISPATCH == 3
  #ifdef storm_WDF_IO_QUEUE_IO_DEVICE_CONTROL
    storm_WDF_IO_QUEUE_IO_DEVICE_CONTROL((WDFQUEUE)&hqueue,&hrequest,(size_t)storm_nondet(),(size_t)storm_nondet(),(ULONG)storm_nondet());
  #elif
    #error Function WDF_IO_QUEUE_IO_DEVICE_CONTROL not defined
  #endif

#elif DISPATCH == 4
  #ifdef storm_WDF_IO_QUEUE_IO_INTERNAL_DEVICE_CONTROL
    storm_WDF_IO_QUEUE_IO_INTERNAL_DEVICE_CONTROL((WDFQUEUE)&hqueue,&hrequest,(size_t)storm_nondet(),(size_t)storm_nondet(),(ULONG)storm_nondet());
  #elif
    #error Function WDF_IO_QUEUE_IO_INTERNAL_DEVICE_CONTROL not defined
  #endif

#elif DISPATCH == 5
  #ifdef storm_WDF_IO_QUEUE_IO_STOP
    storm_WDF_IO_QUEUE_IO_STOP((WDFQUEUE)&hqueue,&hrequest,(ULONG)storm_nondet());
  #elif
    #error Function WDF_IO_QUEUE_IO_STOP not defined
  #endif

#else
  #error Non existent DISPATCH value
#endif
}

void cancel() {
  PFN_WDF_REQUEST_CANCEL cancelRoutine;

  if (storm_nondet()) {
    STORM_ATOMIC(
      __hv_assume(__resource("CANCEL_ROUTINE", &hrequest) == cancelRoutine);
      __hv_updates_resource("CANCEL_STARTED", &hrequest, TRUE);
    );
    cancelRoutine(&hrequest);
  }
}

void completion() {
  PFN_WDF_REQUEST_COMPLETION_ROUTINE completionRoutine;
  WDFCONTEXT completionContext;

  if (storm_nondet()) {
    STORM_ATOMIC(
      __hv_assume(__resource("COMPLETION_ROUTINE", &hrequest) == completionRoutine);
      __hv_assume(__resource("COMPLETION_CONTEXT", &hrequest) == completionContext);
      __hv_assume(__resource("SENT", &hrequest) == TRUE);
    );
    completionRoutine(&hrequest, NULL, NULL, completionContext);
  }
}

void dpc() {
#ifdef storm_WDF_TIMER_1
  storm_WDF_TIMER_1(&htimer);
#endif
}

void completion2() {
  PFN_WDF_REQUEST_COMPLETION_ROUTINE completionRoutine;
  WDFCONTEXT completionContext;

  if (storm_nondet()) {
    STORM_ATOMIC(
      __hv_assume(__resource("COMPLETION_ROUTINE", &created_hrequest) == completionRoutine);
      __hv_assume(__resource("COMPLETION_CONTEXT", &created_hrequest) == completionContext);
      __hv_assume(__resource("SENT", &created_hrequest) == TRUE);
    );
    completionRoutine(&created_hrequest, NULL, NULL, completionContext);
  }
}


#define __global_allocated(global,size) __requires(__allocated(((char*)&global) + size))
__global_allocated(hrequest,sizeof(WDFREQUEST))
__global_allocated(hrctx,200)
__global_allocated(htimer,sizeof(WDFTIMER))
__global_allocated(htctx,200)
__global_allocated(hdevice,sizeof(WDFDEVICE))
__global_allocated(hdctx,200)
__global_allocated(hqueue,sizeof(WDFQUEUE))
__global_allocated(hqctx,200)
__global_allocated(hbuffer,200)
void storm_main ()
{

  // Initialization
  cancelLockStatus == UNLOCKED;

  __hv_assume(__resource("COMPLETED", &hrequest) == FALSE);
  __hv_assume(__resource("CANCEL_ROUTINE", &hrequest) == NULL);
  __hv_assume(__resource("CANCEL_STARTED", &hrequest) == FALSE);
  __hv_assume(__resource("COMPLETION_ROUTINE", &hrequest) == NULL);
  __hv_assume(__resource("COMPLETION_CONTEXT", &hrequest) == NULL);
  __hv_assume(__resource("SENT", &hrequest) == FALSE);
  __hv_assume(__resource("COLLECTION", &hrequest) == NULL);
  __hv_assume(__resource("REFERENCE", &hrequest) == 0);
  __hv_assume(__resource("CONTEXT", &hrequest) == &hrctx);
  __hv_assume(__resource("OBJECT", &hrctx) == &hrequest);

  __hv_assume(__resource("COMPLETED", &created_hrequest) == FALSE);
  __hv_assume(__resource("CANCEL_ROUTINE", &created_hrequest) == NULL);
  __hv_assume(__resource("CANCEL_STARTED", &created_hrequest) == FALSE);
  __hv_assume(__resource("COMPLETION_ROUTINE", &created_hrequest) == NULL);
  __hv_assume(__resource("COMPLETION_CONTEXT", &created_hrequest) == NULL);
  __hv_assume(__resource("SENT", &created_hrequest) == FALSE);
  __hv_assume(__resource("COLLECTION", &created_hrequest) == NULL);
  __hv_assume(__resource("REFERENCE", &created_hrequest) == 0);
  __hv_assume(__resource("CONTEXT", &created_hrequest) == &created_hrctx);
  __hv_assume(__resource("OBJECT", &created_hrctx) == &created_hrequest);

  __hv_assume(__resource("CONTEXT", &htimer) == &htctx);
  __hv_assume(__resource("OBJECT", &htctx) == &htimer);
  __hv_assume(__resource("CONTEXT", &hdevice) == &hdctx);
  __hv_assume(__resource("OBJECT", &hdctx) == &hdevice);
  __hv_assume(__resource("CONTEXT", &hqueue) == &hqctx);
  __hv_assume(__resource("OBJECT", &hqctx) == &hqueue);

  myInitDriver();


  // T1: Dispatch
  __async_call dispatch();

  // T2: Cancel routine
  __async_call cancel();

  // T3: Completion routine
  __async_call completion();

  // T4: Deferred procedure call routine
  __async_call dpc();

  // T5: Completion routine II
  __async_call completion2();
}


void __cdecl main() {}

